%{
#include <stdio.h>
#include <stdlib.h>
#include <stdarg.h>	
%}

%token VLINE STAR PLUS FOR_ALL THERE_EXISTS NOT AND DOUBLE_ARROW RIGHT_ARROW
%token LEFT_ARROW XOR NOR NAND EQUAL_SIGN NOT_EQUAL_SIGN ARROW GENTZEN_ARROW
%token ASSIGN SYMBOL1 SYMBOL2 SYMBOL3 SYMBOL4 SYMBOL5

%token THF FOF CNF AXIOM HYPOTHESIS DEFINITION ASSUMPTION LEMMA THEOREM 
%token CONJECTURE NEGATED_CONJECTURE PLAIN FI_DOMAIN FI_FUNCTORS FI_PREDICATES
%token TYPE UNKNOWN DOLLAR_OTYPE DOLLAR_O DOLLAR_ITYPE DOLLAR_I DOLLAR_TTYPE
%token DOLLAR_REAL DOLLAR_RAT DOLLAR_INT DOLLAR_TRUE DOLLAR_FALSE DOLLAR_EQUAL
%token INFERENCE INTRODUCED AXIOM_OF_CHOICE TAUTOLOGY THEORY 
%token EQUALITY AC CREATOR DESCRIPTION IQUOTE STATUS SUC UNP SAP ESA SAT FSA 
%token THM EQV TAC WEC ETH TAU WTC WTH CAX SCA TCA WCA CUP CSP ECS CSA CTH CEQ 
%token UNC WCC ECT FUN UNS WUC WCT SCC UCA NOC ASSUMPTIONS REFUTATION INCLUDE 
%token DOLLAR_THF DOLLAR_FOF DOLLAR_CNF DOLLAR_FOT

%token unsigned_integer general_function dollar_dollar_word single_quoted real 
%token integer dollar_word lower_word upper_word rational distinct_object

%%

TPTP_file
	: TPTP_inputs
	;
TPTP_inputs
	: TPTP_input
	| TPTP_input TPTP_inputs
	;
TPTP_input
	: annotated_formula 
	| include
	;
annotated_formula
	: thf_annotated 
	| fof_annotated 
	| cnf_annotated
	;
thf_annotated
	: THF '(' name ',' formula_role ',' thf_formula annotations ')' '.'
	;
fof_annotated
	: FOF '(' name ',' formula_role ',' fof_formula annotations ')' '.'
	;
cnf_annotated
	: CNF '(' name ',' formula_role ',' cnf_formula annotations ')' '.'
	;
annotations
	: ',' source optional_info 
	|
	;
formula_role
	: lower_word
	| AXIOM
	| HYPOTHESIS
	| DEFINITION
	| ASSUMPTION
	| LEMMA
	| THEOREM
	| CONJECTURE
	| NEGATED_CONJECTURE
	| PLAIN
	| FI_DOMAIN
	| FI_FUNCTORS
	| FI_PREDICATES
	| TYPE
	| UNKNOWN
	;
thf_formula
	: thf_logic_formula 
	| thf_definition 
	| thf_sequent
	;
thf_logic_formula
	: thf_binary_formula  
	| thf_type_formula
	;
thf_binary_formula
	: thf_binary_tuple 
	| thf_binary_type
	;
thf_binary_tuple
	: thf_unitary_formula
	| thf_binary_tuple thf_pair_connective thf_unitary_formula
	;
thf_unitary_formula
	: thf_quantified_formula 
	| thf_unary_formula 
	| thf_atom				{/* here be problem */} 
	| thf_tuple 
	| thf_letrec 
	| '(' thf_logic_formula ')'
	;
thf_quantified_formula
	: thf_quantifier '[' thf_variable_list ']' ':' thf_unitary_formula
	;
thf_variable_list
	: thf_variable 
	| thf_variable ',' thf_variable_list
	;
thf_variable
	: thf_typed_variable 
	| variable
	;
thf_typed_variable
	: variable ':' thf_top_level_type
	;
thf_unary_formula
	: thf_unary_connective '(' thf_logic_formula ')'
	;
thf_atom
	: term 
	;
thf_tuple
	: '[' ']' 
	| '[' thf_tuple_list ']'
	;
thf_tuple_list
	: thf_tuple_list ',' thf_unitary_formula	{/* swapped these */}
	;
thf_type_formula
	: thf_typeable_formula ':' thf_top_level_type
	;
thf_typeable_formula
	: thf_atom 
	| thf_tuple 
	| '(' thf_logic_formula ')'
	;
thf_top_level_type
	: thf_logic_formula
	;
thf_unitary_type
	: thf_unitary_formula
	;
thf_binary_type
	: thf_mapping_type 
	| thf_xprod_type 
	| thf_union_type
	;
thf_mapping_type
	: thf_unitary_type ARROW thf_unitary_type 
	| thf_unitary_type ARROW thf_mapping_type
	;
thf_xprod_type
	: thf_unitary_type STAR thf_unitary_type 
	| thf_xprod_type STAR thf_unitary_type
	;
thf_union_type
	: thf_unitary_type PLUS thf_unitary_type 
	| thf_union_type PLUS thf_unitary_type
	;
thf_letrec
	: ASSIGN '[' thf_letrec_list ']' ':' thf_unitary_formula
	;
thf_letrec_list
	: thf_defined_var 
	| thf_defined_var ',' thf_letrec_list
	;
thf_defined_var
	: thf_variable ASSIGN thf_logic_formula 
	| '(' thf_defined_var ')'
	;
thf_definition
	: thf_defn_constant ASSIGN thf_logic_formula 
	| '(' thf_definition ')'
	;
thf_defn_constant
	: thf_type_formula
	| constant
	;
thf_sequent
	: thf_tuple GENTZEN_ARROW thf_tuple
	;
fof_formula
	: binary_formula 
	| unitary_formula
	;
binary_formula
	: nonassoc_binary 
	| assoc_binary
	;
nonassoc_binary
	: unitary_formula binary_connective unitary_formula
	;
assoc_binary
	: or_formula 
	| and_formula
	;
or_formula
	: unitary_formula VLINE unitary_formula 
	| or_formula VLINE unitary_formula
	;
and_formula
	: unitary_formula AND unitary_formula 
	| and_formula AND unitary_formula
	;
unitary_formula
	: quantified_formula 
	| unary_formula 
	| atomic_formula 
	| '(' fof_formula ')'
	;
quantified_formula
	: quantifier '[' variable_list ']' ':' unitary_formula
	;
variable_list
	: variable 
	| variable ',' variable_list
	;
unary_formula
	: unary_connective unitary_formula 
	| fol_infix_unary
	;
cnf_formula
	: '(' disjunction ')' 
	| disjunction
	;
disjunction
	: literal 
	| disjunction VLINE literal
	;
literal
	: atomic_formula 
	| NOT atomic_formula 
	| fol_infix_unary
	;
fol_infix_unary
	: term infix_inequality term
	;
thf_quantifier
	: quantifier 
	| SYMBOL1
	| SYMBOL2
	| SYMBOL3
	;
thf_pair_connective
	: infix_equality 
	| infix_inequality 
	| binary_connective
	| assoc_connective
	| '@'
	;
thf_unary_connective
	: unary_connective 
	| SYMBOL4
	| SYMBOL5
	;
quantifier
	: FOR_ALL
	| THERE_EXISTS
	;
binary_connective
	: DOUBLE_ARROW
	| RIGHT_ARROW
	| LEFT_ARROW
	| XOR
	| NOR
	| NAND
	;
assoc_connective
	: VLINE
	| AND
	;
unary_connective
	: NOT
	;
atomic_formula
	: plain_atomic_formula 
	| defined_atomic_formula 
	| system_atomic_formula
	;
plain_atomic_formula
	: plain_term
	;
defined_atomic_formula
	: defined_atomic_term
	| defined_infix_formula
	;
defined_infix_formula
	: term defined_infix_pred term
	;
defined_infix_pred
	: infix_equality
	;
infix_equality
	: EQUAL_SIGN
	;
infix_inequality
	: NOT_EQUAL_SIGN
	;
system_atomic_formula
	: system_term
	;
term
	: function_term 
	| variable
	;
function_term
	: plain_term 
	| defined_term 
	| system_term
	;
plain_term
	: constant 
	| functor '(' arguments ')'
	;
constant
	: functor
	;
functor
	: atomic_word
	;
defined_term
	: defined_atom 
	| defined_atomic_term
	;
defined_atom
	: number 
	| distinct_object
	;
defined_atomic_term
	: defined_plain_term
	;
defined_plain_term
	: defined_constant 
	| defined_functor '(' arguments ')'
	;
defined_constant
	: defined_functor
	;
defined_functor
	: atomic_defined_word
	;
system_term
	: system_constant 
	| system_functor '(' arguments ')'
	;
system_constant
	: system_functor
	;
system_functor
	: atomic_system_word
	;
variable
	: upper_word
	;
arguments
	: term 
	| term ',' arguments
	;
source
	: general_term
	;
optional_info
	: ',' useful_info
	| 
	;
useful_info
	: general_list
	;
include
	: INCLUDE '(' file_name formula_selection ')' '.'
	;
formula_selection
	: ',' '[' name_list ']' 
	|
	;
name_list
	: name 
	| name ',' name_list
	;
general_term
	: general_data 
	| general_data ':' general_term 
	| general_list
	;
general_data
	: atomic_word 
	| atomic_word '(' general_terms ')' 
	| variable 
	| number 
	| distinct_object 
	| formula_data
	;
formula_data
	: DOLLAR_THF '(' thf_formula ')' 
	| DOLLAR_FOF '(' fof_formula ')' 
	| DOLLAR_CNF '(' cnf_formula ')' 
	| DOLLAR_FOT '(' term ')'
	;
general_list
	: '[' ']' 
	| '[' general_terms ']'
	;
general_terms
	: general_term 
	| general_term ',' general_terms
	;
name
	: atomic_word 
	| unsigned_integer
	;
atomic_word
	: lower_word
	| single_quoted
	;
atomic_defined_word
	: dollar_word
	;
atomic_system_word
	: dollar_dollar_word
	;
number
	: integer 
	| rational 
	| real
	; 
file_name
	: single_quoted
	;
%%
